\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros

\newcommand{\ep}[0]{\epsilon} 
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\app}[0]{\mathsf{app}} 

\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}


\begin{document}
%\pagestyle{empty}
\title{$\mathbf{F}_{\omega}$ with Term Universal}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{last edited: \today}


\maketitle
\thispagestyle{empty}
\begin{abstract}
  This note show how one can do Church encoding with a simple extension of $\mathbf{F}_{\omega}$ with term universal $\forall x.T$ and type level comprehension scheme $\lambda x:T'.T$ and $Tt$. It is a suggestion from Prof. Stump based on my previous work on system $\mathfrak{G}$. 
\end{abstract}
 
\section{The System}

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Types} $T \ ::= \ \| \ X \ | \ \Pi X:\kappa.T \ | \ \ T_1 \to T_2 \ | \ \forall x.T \ | \ \iota x.T \ | \ t \ep T $

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T$

\end{definition} 

%% \begin{definition}[Metalevel Abrieviation]
%% \

%%   \noindent \textit{Objects} $o \ ::= \ t \ | \ T$

%%   \noindent \textit{Reduction Context} $\mathcal{C} \ ::=$

%% \noindent $ \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ |\ \Delta X:\kappa.\mathcal{C} \ | \ \Pi x:T .\mathcal{C} \ |\ \Pi x:\mathcal{C}.T \ | \  \forall x:T .\mathcal{C} \ |\ \forall x:\mathcal{C}.T \ | \ \lambda X.\mathcal{C} \ | \ \iota x.\mathcal{C} \ | \ T \mathcal{C} \ | \ \mathcal{C} T \ | \ \xi x:\mathcal{C}.\kappa \ | \  \zeta X:\mathcal{C}. \kappa \ | \ \xi x:\kappa.\mathcal{C} \ | \  \zeta X:\kappa. \mathcal{C}$

%% \end{definition}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 &  T_1 \cong T_2}

&

\infer[\textit{toFormula}]{\Gamma \vdash t: t \ep (\iota x.T)}{\Gamma
\vdash t : \iota x.T}

\\
\\

\infer[\textit{toSet}]{\Gamma\vdash t : \iota x.T}{\Gamma \vdash t: t \ep (\iota x.T)}

&
\infer[\textit{Forall}]{\Gamma \vdash t : \forall x.T}
{\Gamma \vdash t: T &  x \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Instantiate}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x.T}

\\
\\

\infer[\textit{Poly}]{\Gamma \vdash  t :\Pi X.T}
{\Gamma \vdash t: T & X \notin \mathsf{FV}(\Gamma)}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Pi X.T}

&

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : T_1\to T_2}
{\Gamma, x:T_1 \vdash t: T_2}

\\
\\
\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t: T_1 \to T_2 & \Gamma \vdash t': T_1}

\end{tabular}
}
\end{definition}

\noindent \textbf{Note}: $\cong$ is defined as reflexive transitve and symmetric closure of 
$\to_{\beta}\cup \to_{\iota}$.
\begin{definition}[Beta Reductions]

\


\begin{tabular}{ll}

\infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{t \ep (\iota x.T) \to_{\iota} [t/x]T}{}

\end{tabular}
  
\end{definition}

\noindent \textbf{Remarks}: 
\

\begin{itemize}
\item This system is a strict two layer system, namely, we maintain 
term type distinction, a term can never be a type, a type can never be a term. 

\item We do not use the notion of \textit{kinding}. Any type in the type syntactical category
and any term in the term syntactical category are considered well-formed. 

\item We do have a notion of typability, that is why we have typing rules, this allow us to have the flexibility of mentioning a term even it is not typable. We will see this flexibility is essential for us to do external reasoning. 
 
\item All term at the term level will terminate, but when the term at type level does not nesserarily terminate, can not even nesseserily typable at type level. For example, one can have $\cdot \vdash \lambda x.x : \Omega \ep T \to \Omega \ep T$.  
\end{itemize}


\section{Church Encoding}

\begin{definition}[Church Numerals]
\

  \noindent $\mathsf{Nat} := \iota x. \Pi C.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $0\  := \lambda s. \lambda z.z$

\noindent With $s:\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), z: 0 \ep C, n: \mathsf{Nat}$, $0$ is typable to $\mathsf{Nat}$, $\mathsf{S}$ is typable to $\mathsf{Nat} \to \mathsf{Nat}$.
\end{definition}

\begin{definition}[Induction]
\

\noindent  $\mathsf{Id} :  \Pi C. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$

\noindent $\mathsf{Id} := \lambda s. \lambda z. \lambda n. n\ s\ z$

\noindent with $s:\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), z: 0 \ep C, n: m \ep \mathsf{Nat}$.
\end{definition}

\begin{definition}[Addition]
\

\noindent  $\mathsf{add}\ u\ v := \mathsf{Id}\ \mathsf{S}\ v \ u$


\end{definition}

\noindent The typing procedure for addition: let $C$ be $\iota x.\mathsf{Nat}$ for $\mathsf{Id}$, so $\mathsf{Id}: (\mathsf{Nat} \to \mathsf{Nat}) \to \mathsf{Nat} \to \forall m(m \ep \mathsf{Nat} \to \mathsf{Nat})$. Note that $\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat}, v :\mathsf{Nat}$. And $u: \mathsf{Nat} \equiv u \ep \mathsf{Nat}$. 

\noindent This suggests that $\mathsf{Id}$ coincides with $\mathsf{It}$ in system $\mathbf{F}$.

\begin{definition}
  $\mathsf{Void} := \iota x. \Pi C. x \ep C$
\end{definition}

\begin{definition}
  $a = b:= \Pi C. a \ep C \to b \ep C$.
\end{definition}

%% \begin{definition}[Axiom of Extensionality]
%% \

%%   \infer[\textit{Ext}]{a \cong b }{\Gamma \vdash t: a = b}
%% \end{definition}

%% \noindent We will not need axiom of extensionality.  

\begin{definition}
\

\noindent $\mathsf{Unit} := \iota x. x = \mathbf{1}$.

\noindent $\mathbf{1}: \mathsf{Unit} := \lambda u.u$ with $u : \mathbf{1} \ep C$
\end{definition}
\begin{lemma}[Reflexitivity of Equality]
\label{symm}
 There is a $t$ such that $\cdot \vdash t : \forall a. (a = a)$.
\end{lemma}
\begin{proof}
  Obvious.
\end{proof}

\begin{lemma}[Symmetry of Equality]
\label{symm}
 There is a $t$ such that $\cdot \vdash t : \forall a. \forall b. (a = b \to b = a)$.
\end{lemma}
\begin{proof}
  Assume $\Pi C. a\ep C \to b \ep C$(1), we want to show $ b \ep A \to a \ep A$ for any $A$. Instantiate $C$ in (1) with $\iota x.  (x \ep A \to a \ep A)$. By comprehension, we get 
$(a \ep A \to a \ep A) \to (b \ep A \to a \ep A)$. And we know that $a \ep A \to a \ep A$ is derivable in our system, so by MP(modus ponens) we get $b \ep A \to a \ep A$. 
\end{proof}

\begin{lemma}[Transitivity of Equality]
\label{symm}
 There is a $t$ such that $\cdot \vdash t : \forall a. \forall b. \forall c. a = b \to b = c \to a = c$.
\end{lemma}
\begin{proof}
For any $a,b,c$, assume $a = b$($\Pi C. a \ep C \to b \ep C$), $b = c$($\Pi C. b \ep C \to c \ep C$), we want to show $a = c$($ a \ep A \to c \ep A$ for any $A$). One can see that this is by 
syllogism. 
\end{proof}




\begin{theorem}
There is a $t$ such that  $\cdot \vdash t : \forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$. 
\end{theorem}
\begin{proof}
We want to show $\forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$.
 Let $P := \iota x. \mathsf{add}\ x\ 0 = x$. Instantiate $\mathsf{Id}$ with $P$, we get 
$  \forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y) \to\mathsf{add}\ 0\ 0 = 0 \to \forall m. (m \ep \mathsf{Nat} \to m \ep P)$. We just have to inhabit 
$\forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y)$ and $\mathsf{add}\ 0\ 0 = 0$. For the base case, we want to show $\Pi C. \mathsf{add}\ 0\ 0 \ep C \to 0 \ep C$. Assume $\mathsf{add}\ 0\ 0 \ep C$, since $\mathsf{add}\ 0\ 0 \to_{\beta} 0$, by conversion, we get $0 \ep C$. For the step case is a bit complicated, assume $\mathsf{add}\ y\ 0 = y$, we want to show $\mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y$. Since $\mathsf{add}\ y\ 0 \to_{\beta} y\ \mathsf{S}\ 0$, so by conversion we have $y \ \mathsf{S}\ 0 = y$. And $\mathsf{add}\ (\mathsf{S}y)\ 0 \to_{\beta} \mathsf{S}(y \ \mathsf{S}\ 0)$, so we are tring to prove $\mathsf{S}(y \ \mathsf{S}\ 0) = \mathsf{S}y$, which is by lemma \ref{cong}. 
\end{proof}

\begin{theorem}
\label{suc}
  $\cdot \vdash t: \forall m. (m \ep \mathsf{Nat} \to \mathsf{S}m \ep \mathsf{Nat})$.
\end{theorem}
\begin{proof}
  By induction. Let $P:= \iota x. \mathsf{S} x \ep \mathsf{Nat}$. Instantiate $C$ in $\mathsf{Id}$ with $P$, we get $  \forall y . ( \mathsf{S}y\ \ep \mathsf{Nat} \to  \mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat}) \to  \mathsf{S}0 \ep \mathsf{Nat} \to \forall m. (m \ep \mathsf{Nat} \to  \mathsf{S}m \ep \mathsf{Nat})$. So we just need to show $\forall y . ( \mathsf{S}y\ \ep \mathsf{Nat} \to  \mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat})$ and $\mathsf{S}0 \ep \mathsf{Nat}$. The base case is immediate. To show the step case, let us assume $\mathsf{S}y\ \ep \mathsf{Nat}$ for any $y$, we need to show 
$\mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat}$. By comprehension, we are assuming $\Pi C. (\forall y. (y \ep C) \to (\mathsf{S}y) \ep C) \to 0 \ep C \to (\mathsf{S}y) \ep C$ $\dagger$, we want to show $ (\forall y. (y \ep A) \to (\mathsf{S}y) \ep A) \to 0 \ep A \to (\mathsf{S} \mathsf{S} y) \ep A$ for any $A$. Assume $(\forall y. (y \ep A) \to (\mathsf{S}y) \ep A)$(1) and $0 \ep A$, we need to show $(\mathsf{S} \mathsf{S} y) \ep A$. Instantiate $C$ with $A$ in $\dagger$, we get $(\forall y. (y \ep A) \to (\mathsf{S}y) \ep A) \to 0 \ep A \to (\mathsf{S}y) \ep A$. By modus ponens, we get $(\mathsf{S}y) \ep A$. Instantiate $y$ in (1) with $\mathsf{S} y$, we get $\mathsf{S} y \ep A \to \mathsf{S} \mathsf{S} y \ep A$. Thus by modus ponens, we get $\mathsf{S} \mathsf{S} y \ep A$. Thus we exibit such an abstract term $t$. 
\end{proof}


\noindent \textbf{Remarks}:
\begin{itemize}
\item  The proof of theorem \ref{suc} can be represented by term $\mathsf{Id}\ \mathsf{S} \ \suc 0$. So if 
$n \ep \mathsf{Nat}$, both $\mathsf{Id}\ (\mathsf{S}0) \ 0\ n$ and $\mathsf{S}\ n$ have the type $\mathsf{S}n \ep \mathsf{Nat}$. This suggest that proof complexity does get \textit{lost} when we reduce $\mathsf{Id}\ (\mathsf{S}0) \ 0\ n \to_{\beta}^* \mathsf{S}\ n$, but still we have type
preservation, we get a simpler proof of the same formula. 

\item Theorem \ref{suc} can also be expressed at meta-typing level, namely, if $m:\mathsf{Nat}$ (by toFormula rule, we have $m:m\ep \mathsf{Nat}$), then $\suc m : \mathsf{Nat}$(by toFormula rule, we get $\suc m : \suc m \ep \mathsf{Nat}$). This is a feature of Church encoding, to be able to move between
a notion of set and formula, we call it \textit{formula-set reciprocity}, see section \ref{logic} for more
information. 

%% \item  The last two theorems show that we do separate the notion of to \textit{type} a program, and to \textit{prove} some property about it. So to type a program does not nessecarily guarantee it has certain property.   
\end{itemize}


\begin{lemma}[Object-level Conversion]
\label{oconv}
  There is a $t$ such that  $\cdot \vdash t: \forall a. \forall b. \Pi P. ( a \ep P \to a = b \to b \ep P)$. 
\end{lemma}
\begin{proof}
  By modus ponens.
\end{proof}
\begin{theorem}
   There is a $t$ such that $\cdot \vdash t : \forall a. \forall b. (a \ep \mathsf{Nat} \to a = b \to b \ep \mathsf{Nat})$.
\end{theorem}
\begin{proof}
  Let $P := \iota x.x\ep \mathsf{Nat}$ for lemma \ref{oconv}. 
\end{proof}

\begin{theorem}[Unprovability I]
There is no such an $t$ that  $\cdot \vdash t:  1 = 0 \to \mathsf{Void}$. 
\end{theorem}

\begin{proof}
By the erasure theorem, if such $t$ exist, it would implies $(\Pi C. C \to C) \to \Pi X.X$ is 
inhabited. Thus $\Pi X.X$ is inhabited. 
\end{proof}

\begin{theorem}[Unprovability II]
There is no such an $t$ that  $\cdot \vdash t:\mathsf{Void}$. 
\end{theorem}

\noindent Above unprovability suggests that our system as a logic system is seemingly has a drawback same as $\mathbf{F}$, i.e. unable to interpret $0 \not = 1$ properly. We will see that it is actually not the case for our system. 


\section{The Erasure to System $\mathbf{F}$}

\begin{definition}
\

  $F(X) := X$

  $F(T_1 \to T_2) := F(T_1) \to F(T_2)$

  $F(\Pi X.T) := \Pi X.F(T)$

  $F(\forall x.T) := F(T)$

  $F(\iota x.T) := F(T)$

  $F(t \ep T) := F(T)$
\end{definition}

\begin{theorem}
\label{const}
  If $\Gamma \vdash t:T$, then $F(\Gamma) \vdash t:F(T)$. 
\end{theorem}
\begin{proof}
  Simply by induction.
\end{proof}

\section{The Notion of Contradictory}

\begin{definition}
  $\bot := \forall x. \forall y. (x = y)$.
\end{definition}

\noindent The meaning of this definition is obvious, every term is the same. Note that 
the erasure of $F(\bot) \equiv \Pi X. X \to X$. So it is inhabited in System \textbf{F}. But 
can one prove that $\bot$ is uninhabited in our system. 

\begin{theorem}[Logical Complexitivity]
\label{logic}
There is no such an $t$ that  $\cdot \vdash t:\bot$. 
\end{theorem}
\begin{proof}
  By theorem \ref{const}, we know that if there is such an $t$, it must be of the
abstraction form, so $u: x \in C \vdash t' : y \in C$ for any $x, y, C$. And now 
according to our typing rule, there are no ways to construct a term of type $y \in C$
under the assumption that $u : x \in C$. 
\end{proof}

\noindent This theorem show that although computationally, our system is the same as system
\textbf{F}, logically, it is strictly richer, we just identify a property that can not be
inhabited in our system but inhabited in system \textbf{F}. Now with this new notion of \textit{contradictory}, we can prove $0 = 1 \to \bot$.

\begin{theorem}
 There is a term $t$ such that $\cdot \vdash 0 = 1 \to \bot$.
\end{theorem}
\begin{proof}
  Assume $\Pi C. 0 \ep C \to 1 \ep C$ $\dagger$, we want to prove for any $x,y, A$, $ x \ep A \to y \ep A$. Assume $x \ep A$(1). We now instantiate $C$ with $\iota u. (((\lambda n. n\ (\lambda z.y)\ x)\ u) \ep A)$ in $\dagger$. By comprehension and beta reduction, we get $x \ep A \to y \ep A$(2). By modus ponens of (1), (2), we get $y \ep A$. So we just exibit an abstract proof
term $t$.   
\end{proof}

\noindent \textbf{Remarks}: 
\begin{itemize}
\item The theorem above show that at least one axiom of $\textbf{HA}_2$
can be proved in our system and also has a well behaved translation to system $\mathbf{F}$, namely, $F(0 = 1 \to \bot) \equiv (\Pi C. C \to C) \to (\Pi C. C \to C)$. 

\item It also shows that Girard's mapping from \textbf{F} with ``junk'' to \textbf{F} is very
well conceived, because that mapping will map his notion of contradictory, $\Pi X.X$ to $\Pi X. X \to X$, which is exactly the erasure of our notion of contradictory.  
\end{itemize}

\begin{theorem}
 There is a term $t$ such that $\cdot \vdash \forall m. ( m \ep \mathsf{Nat} \to \mathsf{S}m =  m \to \bot)$.
\end{theorem}

\section{Injectivity of $\mathsf{S}$}
\noindent Just as the $\mathsf{pred}$ function for Church numerals is really hard to define, 
proving injectivity in our system is considered the hardest theorem to be proved.

\begin{definition}[Predecessor, Kleene]
$\mathsf{pred} := \lambda n.\lambda f. \lambda x. n \ (\lambda g.\lambda h. h\ (g\ f)) (\lambda u. x) (\lambda u.u)$.  
\end{definition}

\begin{lemma}
\label{tcong}
   $\cdot \vdash t: \forall a. \forall b. (a = b \to \lambda s.\lambda z. s\ (a\ s\ z) = \lambda s.\lambda z. s\ (b\ s\ z))$. 
\end{lemma}
\begin{proof}
Assume $\Pi C. a \ep C \to b \ep C$ $\dagger$, we want to show that $\lambda s.\lambda z. s\ (a\ s\ z) \ep A \to \lambda s.\lambda z. s\ (b\ s\ z) \ep A$ for any $A$. Instantiate $C$ by $\iota x.(\lambda s.\lambda z. s\ (x\ s\ z) \ep A)$ in $\dagger$, by comprehension, we have $\lambda s.\lambda z. s\ (a\ s\ z) \ep A \to \lambda s.\lambda z. s\ (b\ s\ z) \ep A$. 
\end{proof}

\begin{lemma}[Intermediate Result]
\label{inter}
  $\cdot \vdash t: \forall m .(m \ep \mathsf{Nat} \to \lambda f.\lambda x.(m\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f = m)$. 
\end{lemma}

\begin{proof}
  We prove this by induction. Let $P:= \iota q. \lambda f.\lambda x.(q\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f = q$. Instantiate $C$ in $\mathsf{Id}$ with $P$, we get $  \forall y . ( y\ \ep P \to  (\mathsf{S} y)\ep P) \to  0 \ep P \to \forall m. (m \ep \mathsf{Nat} \to  m \ep P)$. We just need to show $0 \ep P$ and $\forall y . ( y\ \ep P \to  (\mathsf{S} y)\ep P)$. For the base case, we want to prove $\lambda f.\lambda x.(0\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f = 0$, this is easily done by evaluation. For the step case, for any $y$, we want to show $y\ \ep P \to  (\mathsf{S} y)\ep P$. Assume $y \ep P$, we need to show $(\mathsf{S} y)\ep P$. By comprehension and beta reduction, we are assuming $\lambda f.\lambda x.(y\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f = y$ (1), we want to show $\lambda f.\lambda x.((\lambda s.\lambda z.s\ (y\ s\ z))\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f = \lambda s.\lambda z.s\ (y\ s\ z)$ (2). By lemma \ref{tcong} and (1), we get $\lambda s.\lambda z.s\ (y\ s\ z) = \lambda s.\lambda z.s\ ((\lambda f.\lambda x.(y\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f)\ s\ z)$ (3). Then by beta reductions we see the right hand side of (3) is Leibniz equals to the left hand side of (2). So by transitivity and symmetry of the equality we prove (2). Thus we exibit the abstract term $t$. 
\end{proof}

\begin{lemma}[Predecessor]
\label{pre}
  $\cdot \vdash t: \forall m . (m \ep \mathsf{Nat} \to \mathsf{pred} (\mathsf{S} m) = m)$.
\end{lemma}
\begin{proof}
Since $\mathsf{pred} (\mathsf{S} m) \to_{\beta}^* \lambda f.\lambda x.(m\ (\lambda g.\lambda h. h\ (g\ f))\ (\lambda u.x))\ f$, by lemma \ref{inter}, we get what we want.  
\end{proof}
\begin{lemma}[Congruence of Equality]
\label{cong}
 There is a $t$ such that $\cdot \vdash t : \forall a. \forall b. \forall f .( a = b \to f\ a = f\ b)$.
\end{lemma}
\begin{proof}
  Assume $\Pi C. a \ep C \to b \ep C$($a = b$). Let $C := \iota x. f x \ep P$ with $P$ free. Instantiate $C$ for the 
assumption, we get $a \ep (\iota x. f x \ep P) \to b \ep (\iota x. f x \ep P)$. By conversion, 
we get $f\ a \ep P \to f\ b \ep P$. So by polymorphic generalization, we get $f\ a = f\ b$. Closing the hypothesis and doing a bunch of generalization, we get what we want.
\end{proof}

\begin{theorem}
  $\cdot \vdash t: \forall n.\forall m. (n \ep \mathsf{Nat} \to m \ep \mathsf{Nat} \to \mathsf{S}m = \mathsf{S}n \to m = n)$. 
\end{theorem}
\begin{proof}
Assume $n \ep \mathsf{Nat}, m \ep \mathsf{Nat}, \mathsf{S}m = \mathsf{S}n$, we want to show $m = n$. Instantiate $a$ with $\mathsf{S}m$, instantiate $b$ with $\mathsf{S}n$, $f$ with $\mathsf{pred}$ in lemma \ref{cong}. By modus ponens, we have $\mathsf{pred}(\mathsf{S}m) = \mathsf{pred}(\mathsf{S}n)$. Thus by lemma \ref{pre}, we have $m = n$.
\end{proof}

\noindent \textbf{Remarks}: The prove of this theorem really benefits a lot from that we do not 
need to type the $\mathsf{pred}$ function(even we may be able to type it, but we do not need to).

\section{Logical Remarks}
\label{logic}
\noindent After conquering Peano's 9 axioms, let me try to illustrate the consequence of this project: The picture of Girard's translation of $\mathbf{HA}_2 \to \mathbf{F}$ can be enriched by this picture: $\mathbf{HA}_2 \to \mathfrak{G} \to \mathbf{F}$, even can be relaced by this picture $\mathfrak{G} \to \mathbf{F}$, since the system $\mathfrak{G}$ encompasses $\mathbf{HA}_2$.

 Philosophically, system $\mathfrak{G}$ is an attempt to show how Frege and Russell's logicism\cite{hatcher:1982} can be adopted in the context of type assignment system \`a la Curry, meaning, reducing the ontology of natural numbers(metaphysical object) to the principle of comprehension and a few logical rules. 

\textbf{Formula-Set Reciprocity}: For Church numerals, we can see that the proof of $\bar{n} \ep \mathsf{Nat}$ coincides with $\bar{n}$. This motivates we add the toFormula and toSet rules, to be able to express the notion of reciprocity. With formula-set reciprocity, we can type $\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat}$. And with $\bar{n}: \mathsf{Nat}$, we can use toFormula rule to go back to $\bar{n} \ep \mathsf{Nat}$.  However, not every encoding system can exploit this property, for example, Scott encoding. We will show in appendix that in fact we can prove for Scott numerals $\bar{n}, \mathsf{Nat}$, we have $\cdot \vdash t: \bar{n} \ep \mathsf{Nat}$, but the $t$ and $\bar{n}$ are not coincide anymore. So for Scott numerals, we can not
use formula-set reciprocity. But system $\mathfrak{G}$ is still have the ability to reason 
about the functions that defined on Scott numerals. As we shall see in the appendix. 

\bibliographystyle{plain}
\bibliography{fomegaM}
\appendix

\section{Scott Encoding}

\begin{definition}[Scott numerals]
  \noindent $\mathsf{Nat} := \iota x. \Pi C.(\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C  \to x \ep C$

\noindent $\mathsf{S} \ := \lambda n. \lambda s.\lambda z. s \ n$

\noindent $0\  := \lambda s. \lambda z.z$

\end{definition}

\noindent \textbf{Note}:  $0$ is typable to $\mathsf{Nat}$, but $\mathsf{S}$ is not typable to $\mathsf{Nat} \to \mathsf{Nat}$. Also note that the proof of $1 \ep \mathsf{Nat}$ is actually Church numerals 1 ! This explain why Church numerals are special, it is in a sense \textit{initial}, meaning, any kind of encoding of $\bar{n}, \mathsf{Nat}$, as long as the definition of $\mathsf{Nat}$ has the same form as Church encoding, then the proof of $\bar{n} \ep \mathsf{Nat}$ will
be Church numeral $n$. 


\begin{definition}[Induction]
\

\noindent  $\mathsf{Id} :  \Pi C. (\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C)) \to 0 \ep C \to \forall m. (m \ep \mathsf{Nat} \to m \ep C)$

\noindent $\mathsf{Id} := \lambda s. \lambda z. \lambda n. n\ s\ z$

\noindent with $s:\forall y . ( (y \ep C) \to (\mathsf{S} y) \ep C), z: 0 \ep C, n: m \ep \mathsf{Nat}$.
\end{definition}

\begin{theorem}
  $\cdot \vdash t : 0 \ep \mathsf{Nat}$.
\end{theorem}
\begin{proof}
  Obvious.
\end{proof}

\begin{theorem}

  $\cdot \vdash t: \forall m. (m \ep \mathsf{Nat} \to \mathsf{S}m \ep \mathsf{Nat})$.
\end{theorem}
\begin{proof}
  By induction. Let $P:= \iota x. \mathsf{S} x \ep \mathsf{Nat}$. Instantiate $C$ in $\mathsf{Id}$ with $P$, we get $  \forall y . ( \mathsf{S}y\ \ep \mathsf{Nat} \to  \mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat}) \to  0 \ep \mathsf{Nat} \to \forall m. (m \ep \mathsf{Nat} \to  \mathsf{S}m \ep \mathsf{Nat})$. So we just need to show $\forall y . ( \mathsf{S}y\ \ep \mathsf{Nat} \to  \mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat})$ and $0 \ep \mathsf{Nat}$. The base case is immediate. To show the step case, let us assume $\mathsf{S}y\ \ep \mathsf{Nat}$ for any $y$, we need to show 
$\mathsf{S}(\mathsf{S} y)\ep \mathsf{Nat}$. By comprehension, we are assuming $\Pi C. (\forall y. (y \ep C) \to (\mathsf{S}y) \ep C) \to 0 \ep C \to (\mathsf{S}y) \ep C$ $\dagger$, we want to show $ (\forall y. (y \ep A) \to (\mathsf{S}y) \ep A) \to 0 \ep A \to (\mathsf{S} \mathsf{S} y) \ep A$ for any $A$. Assume $(\forall y. (y \ep A) \to (\mathsf{S}y) \ep A)$(1) and $0 \ep A$, we need to show $(\mathsf{S} \mathsf{S} y) \ep A$. Instantiate $C$ with $A$ in $\dagger$, we get $(\forall y. (y \ep A) \to (\mathsf{S}y) \ep A) \to 0 \ep A \to (\mathsf{S}y) \ep A$. By modus ponens, we get $(\mathsf{S}y) \ep A$. Instantiate $y$ in (1) with $\mathsf{S} y$, we get $\mathsf{S} y \ep A \to \mathsf{S} \mathsf{S} y \ep A$. Thus by modus ponens, we get $\mathsf{S} \mathsf{S} y \ep A$. Thus we exibit such an abstract term $t$. 
\end{proof}

\noindent I directly copy the proof of theorem \ref{suc} without any changes, this move suggests that as long as the proof is \textit{pure}, i.e. does not use rule toFormula and toSet, then
it is basically can be carried directly to Scott numerals. 

\begin{definition}[Recursive Equation]
  $\mathsf{add} :=  \lambda n. \lambda m.n\ (\lambda p. \mathsf{add}\ p\ (\mathsf{S} m))\ m$
\end{definition}

\noindent We know that the above recursive equation can be solved by fixpoint. But we do not 
bother to solve it. The way we treat it is use it as a kind of build in beta equality, when
every we see a $\mathsf{add}$, we one step unfold it. 

\begin{theorem}
There is a $t$ such that  $\cdot \vdash t : \forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$. 
\end{theorem}
\begin{proof}

We want to show $\forall n. (n \ep \mathsf{Nat} \to \mathsf{add}\ n\ 0 = n)$.
 Let $P := \iota x. \mathsf{add}\ x\ 0 = x$. Instantiate $\mathsf{Id}$ with $P$, we get 
$  \forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y) \to\mathsf{add}\ 0\ 0 = 0 \to \forall m. (m \ep \mathsf{Nat} \to m \ep P)$. We just have to inhabit 
$\forall y . ( \mathsf{add}\ y\ 0 = y \to \mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y)$ and $\mathsf{add}\ 0\ 0 = 0$. For the base case, we want to show $\Pi C. \mathsf{add}\ 0\ 0 \ep C \to 0 \ep C$. Assume $\mathsf{add}\ 0\ 0 \ep C$, since $\mathsf{add}\ 0\ 0 \to_{\beta} 0$, by conversion, we get $0 \ep C$. For the step case is a bit complicated, assume $\mathsf{add}\ y\ 0 = y$, we want to show $\mathsf{add}\ (\mathsf{S} y)\ 0 = \mathsf{S} y$. Since $\mathsf{add}\ y\ 0 \to_{\beta} y\ (\lambda p.\mathsf{add}\ p\ (\suc 0))\ 0$,  And $\mathsf{add}\ (\mathsf{S}y)\ 0 \to_{\beta} \mathsf{add} \ y \ (\suc 0) \leftarrow_{\beta}^* \suc (\mathsf{add}\ y\ 0)$. So lemma \ref{cong} will give us this. 
\end{proof}

\begin{definition}
  $\mathsf{pred} := \lambda n.n\ (\lambda p.p)\ 0$
\end{definition}


\section{Dependent Product}

We extend $\mathfrak{G}$ with three new type construct: $\Pi x:T.T'$ and $T\ t, \lambda x.T$ andreplace the Func and App rule with the following two new typing rules: 

\

\begin{tabular}{ll}
\infer[\textit{Indx}]{\Gamma \vdash \lambda x.t : \Pi x: T_1.T_2}
{\Gamma, x:T_1 \vdash t: T_2}

&
\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t: \Pi x:T_1.T_2 & \Gamma \vdash t': T_1}
  
\end{tabular}

\

\noindent And we need another type level reduction rule:

\infer{(\lambda x.T)t \to_{\beta} [t/x]T}{}
 
\noindent We also write $T_1 \to T_2$ if $x \notin \mathsf{FV}(T_2)$ for $\Pi x:T_1.T_2$. 

\noindent \textbf{Remarks}
\begin{itemize}
\item  We want to investigate index product because we want to see if it is possible to obtain formula-set reciprocity for vector data type, which is canon in dependent type programming language. In this section we assume natural numbers as Church numerals.

\item We want to identify three kinds of quantification, $\forall x.T$,  $\Pi x:T_1.T_2$ and $\forall x. x \ep T_1 \to T_2$. The first one is strongest in the sense that it quantifies over all term; the second one quantifies over all terms of type $T_1$, the third one quantifies over the terms that has a self type $T_1$. 
\end{itemize}

\

\begin{definition}[Vector]
\

\noindent  $\mathsf{vec}(U, n) := \iota x. \Pi C. (\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep C m \to (\mathsf{cons}\ m\ u\ y) \ep C (\mathsf{S}m))) \to \mathsf{nil} \ep C 0 \to x \ep C n$

\noindent $\nil := \lambda y. \lambda x.x : \vecc(U, 0)$

\noindent $\cons := \lambda n.\lambda v. \lambda l. \lambda y. \lambda x.y \ n\ v\ (l \ y\ x) : \Pi n: \mathsf{Nat}.U \to \vecc (U, n) \to \vecc (U, \suc n)$.

\noindent where $n: \mathsf{Nat}, v: U, l: \vecc (U, n), y:\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep C m \to (\mathsf{cons}\ m\ u\ y) \ep C (\mathsf{S}m)), x: \nil \ep C0 $. 


\end{definition}

\begin{proof}
\noindent It is easy to see that $\nil$ is typable to $\vecc (U, 0)$. Now we show how $\cons$ is typable to $\Pi n: \mathsf{Nat}.U \to \vecc (U, n) \to \vecc (U, \suc n)$. We can see that $l\ y\ x: l \ep C n$. After the instantiation, the type of $y \ n\ v:  l \ep C n \to (\mathsf{cons}\ n\ v\ l) \ep C (\mathsf{S}n)$. So $y\ n\ v \ (l\ y\ x): (\mathsf{cons}\ n\ v\ l) \ep C (\mathsf{S}n)$. So $\lambda y. \lambda x. y\ n\ v \ (l\ y\ x) : \Pi C. (\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep C m \to (\mathsf{cons}\ m\ u\ y) \ep C (\mathsf{S}m))) \to  \nil \ep C0 \to  \lambda y. \lambda x. y\ n\ v \ (l\ y\ x) \ep C(\suc n)$. So $\lambda y. \lambda x. y\ n\ v \ (l\ y\ x) : \vecc (U, \suc n)$. So $ \cons : \Pi n:\mathsf{Nat}. U \to \vecc(U, n) \to \vecc(U, \suc n)$.
  
\end{proof}


\noindent The above development suggests that dependent type can be included in the framework
of system $\mathfrak{G}$ and we just need to modify the erasure function $F(\Pi x:T_1.T_2) := F(T_1) \to F(T_2)$ and $F(T t) := F(T)$ and $F(\lambda x.T) = F(T)$, then we still can go back to system \textbf{F}. More importantly, our vector encoding has the formula-set reciprocity, this is a highly desirable property that 
enable us to do dependent programming effectively in $\mathfrak{G}$. 

\begin{definition}[Induction Principle]
\

  \noindent  $\mathsf{ID}(U, n) := \Pi C. (\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep C m \to (\mathsf{cons}\ m\ u\ y) \ep C (\mathsf{S}m))) \to \mathsf{nil} \ep C 0 \to \forall x(x \ep \vecc(U,n) \to x \ep Cn)$

\noindent $\mathsf{ID}(U,n) := \lambda s. \lambda z. \lambda n. n\ s\ z$

\noindent Let $s : (\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep C m \to (\mathsf{cons}\ m\ u\ y) \ep C (\mathsf{S}m))), z: \mathsf{nil} \ep C 0, n: x \ep \vecc(U,n)$
\end{definition}

\begin{definition}[append]
\

\noindent $\app := \lambda n_1. \lambda n_2. \lambda l_1. \lambda l_2. l_1\ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v)\ l_2$.

\noindent For $n+n_2$ we mean $\mathsf{add}\ n\ n_2$. We can use induction to define append
as well.

\noindent $\app := \lambda n_1. \lambda n_2. \mathsf{ID}(U, n_1) (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v)\ l_2 \ l_1$. 
\end{definition}

\begin{proof}
  We want to show $\app : \Pi n_1:\mathsf{Nat}. \Pi n_2:\mathsf{Nat}. \vecc(U, n_1) \to \vecc(U, n_2) \to \vecc(U, n_1+n_2)$. Observe that $\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v: \Pi n:\mathsf{Nat}. \Pi x:U. v \ep \vecc(U, n+n_2) \to \vecc(U, n+n_2+1) $. We instantiate $C :=  \lambda y.(\iota x.\vecc(U, y + n_2))$ , where $x$ free over $\vecc(U, y + n_2)$, in $\mathsf{ID}(U, n_1)$, by comprehension and beta reductions, we get $\mathsf{ID}(U, n_1) : \forall y. (\Pi m: \mathsf{Nat}. \Pi u:U.  \vecc(U, m+n_2) \to  \vecc (U, \mathsf{S}m+n_2)) \to \vecc(U, 0+n_2)  \to \forall x(x \ep \vecc(U,n_1) \to  \vecc(U, n_1+n_2))$. So $\mathsf{ID}(U, n_1) \ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v) : \vecc(U, 0+n_2)  \to \forall x(x \ep \vecc(U,n_1) \to  \vecc(U, n_1+n_2))$. Of course we assume $l_1: \vecc(U, n_1), l_2:\vecc(U, n_2)$, so $\mathsf{ID}(U, n_1) \ (\lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v) \ l_2 \ l_1: \vecc(U, n_1+n_2)$. 
\end{proof}

\begin{theorem}[Associativity]
  $\cdot \vdash t: \forall (n_1. n_2. n_3. v_1. v_2.v_3). (n_1 \ep \mathsf{Nat} \to n_2 \ep \mathsf{Nat} \to n_3 \ep \mathsf{Nat} \to v_1 \ep \vecc(U, n_1) \to v_2 \ep \vecc(U, n_2)) \to v_3 \ep \vecc(U, n_3) \to \app \ n_1\ (n_2+n_3)\ v_1 \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (n_1 + n_2) \ n_3\ (\app \ n_1 \ n_2 \ v_1 \ v_2) \ v_3$
\end{theorem}

\begin{proof}
  Assume $x_1: n_1 \ep \mathsf{Nat}, x_2: n_2 \ep \mathsf{Nat}, x_3: n_3 \ep \mathsf{Nat}, y_2: v_2 \ep \vecc(U, n_2)) , y_3: v_3 \ep \vecc(U, n_3)$. We want to show $\forall v_1. (v_1 \ep \vecc(U, n_1) \to \app \ n_1\ (n_2+n_3)\ v_1 \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (n_1 + n_2) \ n_3\ (\app \ n_1 \ n_2 \ v_1 \ v_2) \ v_3)$. Let $P:= \lambda z.\iota y. (\app \ z\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (z + n_2) \ n_3\ (\app \ z \ n_2 \ y \ v_2) \ v_3)$. We instantiate the $C$ in $\mathsf{ID}(U,n_1)$ with $P$, we have $\mathsf{ID}(U,n_1):  (\forall y. (\Pi m: \mathsf{Nat}. \Pi u:U. y \ep P m \to (\mathsf{cons}\ m\ u\ y) \ep P (\mathsf{S}m))) \to \mathsf{nil} \ep P 0 \to \forall x(x \ep \vecc(U,n_1) \to x \ep P n_1)$. So we just need to prove base case: $\app \ 0\ (n_2+n_3)\ \nil \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (0 + n_2) \ n_3\ (\app \ 0 \ n_2 \ \nil \ v_2) \ v_3$ and step case: $\Pi m: \mathsf{Nat}. \Pi u:U.  (\app \ m\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (m + n_2) \ n_3\ (\app \ m \ n_2 \ y \ v_2) \ v_3)\to (\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (\suc m + n_2) \ n_3\ (\app \ \suc m \ n_2 \ (\mathsf{cons}\ m\ u\ y) \ v_2) \ v_3)$. For the base case, $\app \ 0\ (n_2+n_3)\ \nil \ (\app\ n_2\ n_3 \ v_2 \ v_3) \to_{\beta}^* \app\ n_2\ n_3 \ v_2 \ v_3 \leftarrow_{\beta}^* \app \ (0 + n_2) \ n_3\ (\app \ 0 \ n_2 \ \nil \ v_2) \ v_3$. For the step case, we assume $\app \ m\ (n_2+n_3)\ y \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (m + n_2) \ n_3\ (\app \ m \ n_2 \ y \ v_2) \ v_3$(IH), we want to show $\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) = \app \ (\suc m + n_2) \ n_3\ (\app \ \suc m \ n_2 \ (\mathsf{cons}\ m\ u\ y) \ v_2) \ v_3$(Goal). We know that $\app \ \suc m\ (n_2+n_3)\ (\mathsf{cons}\ m\ u\ y) \ (\app\ n_2\ n_3 \ v_2 \ v_3) \to_{\beta}^* \cons\ (m+n_2+n_3)\ u \ (y\ \mathcal{X}\ (\app\ n_2\ n_3 \ v_2 \ v_3))$, where $\mathcal{X}:= \lambda n. \lambda x.\lambda v. \cons  (n+n_2+n_3)\ x\ v$. The left hand side of (IH) can be beta reduced to $(y\ \mathcal{X}\ (\app\ n_2\ n_3 \ v_2 \ v_3))$. The right hand side of the (Goal) can be reduced to $\app \ (\suc m + n_2) \ n_3 (\cons\ (m+n_2)\ u \ (y\ \mathcal{C}\ v_2)) v_3 \to_{\beta}^* \cons \ (m+n_2+n_3) \ u \ ((y\ \mathcal{C}\ v_2) \ \mathcal{Q}\ v_3)$, where $\mathcal{C}:= \lambda n. \lambda x.\lambda v. \cons  (n+n_2)\ x\ v, \mathcal{Q}:= \lambda n. \lambda x.\lambda v. \cons  (n+n_3)\ x\ v$. The right hand side of (IH) can be reduced to $((y\ \mathcal{C}\ v_2) \ \mathcal{Q}\ v_3)$. 
So (IH) can be simplified to $y\ \mathcal{X}\ (\app\ n_2\ n_3 \ v_2 \ v_3) = (y\ \mathcal{C}\ v_2) \ \mathcal{Q}\ v_3$. Congruence over the $f:= \cons \ (m+n_2+n_3) \ u$ give us the (Goal). 
\end{proof}

\section{Reflection}
Now it is a good place to stop and ask ourself what does all this implies, instead of going ahead and prove more theorems. 

All the encoding we have done so far, it is about \textit{inductive} describable set. If we are 
able to describe a set using the scheme similar to $\mathsf{Nat}, \vecc$, then by formula-set reciprocity, any term has this set as type will be data of this set. How hard is it to find out 
what kind of element of this set has, it turns out it is not very hard, once the description is
done, one can erase the description over to system \textbf{F}, then any one of the inhabitant of
this system \textbf{F} type will do. So \textit{all} data of inductive describable set has computation meaning. 

For the non-inductive describable ones, we can still \textit{reasoning} about them \textit{externally}, but the proof of them will not have the computational meaning any more, so it is acceptable to add more features(classical axioms, etc.) to enhance reasoning of this kind of sets.  


\end{document}
